package ch.epfl.lara.matcheck.verify;

import ch.epfl.lara.matcheck.ast.{SetExpr,Union,Intersection,Set}

trait SetFormulaMaker extends AbstractFormulaMaker {

  /**
   * <p>
   *        Infix the intersect operator between each element of the <code>sets</code>. 
   * </p>
   *  
   * @param sets: A List of set.
   * @return    : A formula set expression.
   */
  protected def intersect(sets: List[Set]): SetExpr = 
    super.connectElements[SetExpr](Intersection)(sets)
  
  
  /**
   * <p>
   *         Infix the union operator between each element of the <code>sets</code>. 
   * </p>
   *  
   * @param sets: A List of set.
   * @return    : A formula set expression.
   */
  protected def union(sets: List[Set]): SetExpr = 
    super.connectElements[SetExpr](Union)(sets)
    
    
  
  /**
   *   <p> 
   *      Create a formula that express that two sets have no elements in common. 
   *  </p>
   *
   * @parameter neg : The negation operator.
   * @parameter and : The conjunction operator.
   * @param setA    : A first set.
   * @param setB    : A second set.  
   * @return            : The formula. 
   */
  protected def disjointUnion[T](neg: T => T, and: (T,T) => T) (setA: T, setB: T): T = neg(and(setA,setB))
  
  
  
  
  /**
   *   <p> 
   *    From a list of sets create a List of formulae such that each of them express that it 
   *        doesn't exists an element that is shared between any two sets. 
   *        The list of sets is gave in argument.  
   *  </p>
   *
   * @parameter disjonctionFunction: The function used to create a formula as ~(A & B). 
   * @param sets                   : The list of sets.
   * @return                       : The list of formulae. 
   */
  protected def disjoint[S,T](disjointUnionFunction: (S,S) => T) (sets: List[S]): List[T] = {
    val length = sets.length
    for(i<-List.range(0,length); 
        j<-List.range(i+1,length)) yield disjointUnionFunction(sets(i),sets(j))
  }

}
